(set-logic ALL)
(set-info :status sat)
(declare-sort R 0)
(declare-fun m (R R) Bool)
(declare-fun e () R)
(declare-fun t () R)
(declare-fun v () Real)
(declare-fun x () R)
(assert (= (m x e) (distinct (m x t) (m x x))))
(assert (= v (sin 1.0)))
(check-sat)
